Nuprl Definition : case_tree_node 4,23

Case tree_node(x) => body(xcont(x1,z)
== (x1.inr(x2 body(hd((x2.tl(x1)))) ; cont(hd(x1),z))([x1]) 
latex



clarification:

Case tree_node(x) => body(xcont(x1,z)
== (x1.inr(x2 body(hd((x2.tl(x1)))) ; cont(hd(x1),z))(x1.nil) 
latex


DefinitionsCase tree_node(x) => body(xcont, inr(x body(x) ; cont, tl(l), hd(l)
FDL editor aliasescase_tree_node

origin